Nuprl Lemma : hd_map
4,23
postcript
pdf
T
,
T'
:Type,
a
:
T
List
,
f
:(
T
T'
). hd(map(
f
;
a
)) =
f
(hd(
a
))
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
A
List
,
||
as
||
,
i
j
,
P
Q
,
False
,
A
,
A
B
,
hd(
l
)
Lemmas
listp
properties
,
ge
wf
,
length
wf1
,
listp
wf
origin
T, T':Type, a:T List
, f:(T
T'). hd(map(f;a)) = f(hd(a)) T, T':Type, a:T List, f:(TT'). hd(map(f;a)) = f(hd(a)) 
Tx:A. B(x)
j
Q
A
B